Prop-EqNoEliminator.agda:8,14-18
Cannot split on datatype in Prop unless target is in Prop
when checking that the pattern refl has type x ≡P y
